Library triangle_midpoints

Require Import PointsType.
Require Import incidence.
Require Import midpoint.
Require Import congruence.

Section Triangle.

Context `{M:triangle_theory}.

Lemma triangle_midpoint : ∀ A B C,
 parallel (line (midpoint A B) (midpoint A C)) (line B C).
Proof.
intros.
destruct A;destruct B;destruct C.
simpl.
ring.
Qed.

Lemma midpoint_cong : ∀ A B,
 let I := midpoint A B in
  cong A I I B.
Proof.
intros.
destruct A;destruct B.
unfold I.
unfold cong.
unfold bar_of_tri.
simpl.
unfold SA, SB, SC.
simpl.
ring.
Qed.

Lemma triangle_midpoint_cong : ∀ A B C,
  cong (midpoint A B) (midpoint A C) (midpoint B C) C.
Proof.
intros.
destruct A;destruct B;destruct C.
unfold cong, midpoint, dist, bar_of_tri.
simpl.
ring.
Qed.

End Triangle.